Analyzing and debugging complex programs using a technique called model checking, is an important process to ensure that a program meets its design goals during and after development thereof. However, a sophisticated program can be challenging to analyze, particularly when the program includes multiple threads which are run in cyclic state spaces.
Multi-thread programs are characterized by including two or more threads which, when executed by an operating system, require processor resource allocation by the operating system. For example, a program may include two threads (t, u). During an execution of the program, thread t may be executed during a first resource allocation, and thread u may be executed during a second resources allocation and so forth, such that the resource allocation may look like: t, u, t, u, u, t, u, . . . t. Unlike acyclic programs, multi-thread cyclic programs may include an indefinite number of resource allocation sequences, thus making it impossible to test each combination of thread executions.
Prior attempts to analyze computer programs include tracking the state of a modified program to determine interactions at each state. More recently, stateless model checking has introduced a type of model checking whereby the model checker explores the state space of the program without capturing the individual program states. The program is executed under the control of a special scheduler that controls all non-determinism in the program. However, prior art stateless model checking only applies to terminating programs which have acyclic state spaces.
Another stateless approach uses a predetermined and arbitrary bound depth to artificially terminate a non-terminating program, thus making it act like a terminating program. This is disadvantageous because it reduces the coverage of a safety verification, thus may not explore a cycle deep enough to uncover improper or undesirable program execution. Conversely, increasing the depth bound increases the inefficiency of a search by exponentially adding more resources to unroll cycles in the state space rather than explore new state spaces.